$\forall$$B$:Type, $P$:($B$$\rightarrow\mathbb{P}$). $\Box$!$P$ $\in$ ($B$$\rightarrow$Type)$\rightarrow\mathbb{P}$